1  /-
  2  Copyright (c) 2018 Patrick Massot. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Patrick Massot, Johannes Hölzl
  5  
  6  Continuous linear functions -- functions between normed vector spaces which are bounded and linear.
  7  -/
  8  import algebra.field
src         └───────────┘
  9  import analysis.normed_space.operator_norm
src         └─────────────────────────────────┘
 10  
 11  noncomputable theory
 12  open_locale classical filter
 13  
 14  open filter (tendsto)
 15  open metric
 16  
 17  variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 18  variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
 19  variables {F : Type*} [normed_group F] [normed_space 𝕜 F]
 20  variables {G : Type*} [normed_group G] [normed_space 𝕜 G]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
 21  
 22  set_option class.instance_max_depth 70
doc             └──────────────────────┘
 23  
 24  /-- A function `f` satisfies `is_bounded_linear_map 𝕜 f` if it is linear and satisfies the
 25  inequality `∥ f x ∥ ≤ M * ∥ x ∥` for some positive constant `M`. -/
 26  structure is_bounded_linear_map (𝕜 : Type*) [normed_field 𝕜]
 27    {E : Type*} [normed_group E] [normed_space 𝕜 E]
 28    {F : Type*} [normed_group F] [normed_space 𝕜 F] (f : E → F)
 29    extends is_linear_map 𝕜 f : Prop :=
 30  (bound : ∃ M, 0 < M ∧ ∀ x : E, ∥ f x ∥ ≤ M * ∥ x ∥)
id                                    
src                                          
typ                                   
 31  
 32  lemma is_linear_map.with_bound
 33    {f : E → F} (hf : is_linear_map 𝕜 f) (M : ℝ) (h : ∀ x : E, ∥ f x ∥ ≤ M * ∥ x ∥) :
id                     └───────────┘                                 
src                      └───────────┘                                        
typ                    └───────────┘                                 
 34    is_bounded_linear_map 𝕜 f :=
id     └───────────────────┘  
src    └───────────────────┘
typ    └───────────────────┘  
doc    └───────────────────┘
 35  ⟨ hf, classical.by_cases
id     └┘  └────────────────┘
src        └────────────────┘
typ    └┘  └────────────────┘
 36    (assume : M ≤ 0, ⟨1, zero_lt_one, assume x,
id                        └─────────┘         
src                        └─────────┘
typ                       └─────────┘         
 37      le_trans (h x) $ mul_le_mul_of_nonneg_right (le_trans this zero_le_one) (norm_nonneg x)⟩)
id       └──────┘       └────────────────────────┘  └──────┘ └──┘ └─────────┘   └─────────┘ 
src      └──────┘         └────────────────────────┘  └──────┘      └─────────┘   └─────────┘
typ      └──────┘       └────────────────────────┘  └──────┘ └──┘ └─────────┘   └─────────┘ 
 38    (assume : ¬ M ≤ 0, ⟨M, lt_of_not_ge this, h⟩)⟩
id                        └──────────┘ └──┘  
src                         └──────────┘
typ                       └──────────┘ └──┘  
 39  
 40  /-- A continuous linear map satisfies `is_bounded_linear_map` -/
 41  lemma continuous_linear_map.is_bounded_linear_map (f : E →L[𝕜] F) : is_bounded_linear_map 𝕜 f :=
id                                                           └─┘     └───────────────────┘  
src                                                           └─┘       └───────────────────┘
typ                                                          └─┘     └───────────────────┘  
doc                                                           └─┘       └───────────────────┘
 42  { bound := f.bound,
id              └────┘
src              └────┘
typ             └────┘
 43    ..f.to_linear_map }
id       └────────────┘
src       └────────────┘
typ      └────────────┘
 44  
 45  namespace is_bounded_linear_map
 46  
 47  /-- Construct a linear map from a function `f` satisfying `is_bounded_linear_map 𝕜 f`. -/
 48  def to_linear_map (f : E → F) (h : is_bounded_linear_map 𝕜 f) : E →ₗ[𝕜] F :=
id                                    └───────────────────┘       └─┘ 
src                                     └───────────────────┘          └─┘ 
typ                                   └───────────────────┘       └─┘ 
doc                                     └───────────────────┘
 49  (is_linear_map.mk' _ h.to_is_linear_map)
id    └───────────────┘   └───────────────┘
src   └───────────────┘    └───────────────┘
typ   └───────────────┘   └───────────────┘
 50  
 51  /-- Construct a continuous linear map from is_bounded_linear_map -/
 52  def to_continuous_linear_map {f : E → F} (hf : is_bounded_linear_map 𝕜 f) : E →L[𝕜] F :=
id                                                └───────────────────┘       └─┘ 
src                                                 └───────────────────┘          └─┘ 
typ                                               └───────────────────┘       └─┘ 
doc                                                 └───────────────────┘          └─┘ 
 53  { cont := let ⟨C, Cpos, hC⟩ := hf.bound in linear_map.continuous_of_bound _ C hC,
id             └─┘          └┘     └┘└────┘    └────────────────────────────┘
src                                   └────┘    └────────────────────────────┘
typ            └─┘          └┘     └┘└────┘    └────────────────────────────┘
 54    ..to_linear_map f hf}
id       └───────────┘  └┘
src      └───────────┘
typ      └───────────┘  └┘
doc      └───────────┘
 55  
 56  lemma zero : is_bounded_linear_map 𝕜 (λ (x:E), (0:F)) :=
id                └───────────────────┘              
src               └───────────────────┘
typ               └───────────────────┘              
doc               └───────────────────┘
 57  (0 : E →ₗ F).is_linear.with_bound 0 $ by simp [le_refl]
id         └┘  └───────┘ └────────┘               └─────┘
src         └┘   └───────┘ └────────┘         └────┘└─────┘└─
typ        └┘  └───────┘ └────────┘         └────┘└─────┘└─
doc                                           └────┘       └─
txt                                           └────┘       └─
par                                           └────┘       └─
pid                                                      
st                                           └───────────────
 58  
src  
typ  
doc  
txt  
par  
pid  
st   
 59  lemma id : is_bounded_linear_map 𝕜 (λ (x:E), x) :=
id              └───────────────────┘           
src             └───────────────────┘
typ             └───────────────────┘           
doc             └───────────────────┘
 60  linear_map.id.is_linear.with_bound 1 $ by simp [le_refl]
id   └───────────┘└────────┘└─────────┘              └─────┘
src  └───────────┘└────────┘└─────────┘        └────┘└─────┘└─
typ  └───────────┘└────────┘└─────────┘        └────┘└─────┘└─
doc                                            └────┘       └─
txt                                            └────┘       └─
par                                            └────┘       └─
pid                                                       
st                                            └───────────────
 61  
src  
typ  
doc  
txt  
par  
pid  
st   
 62  lemma fst : is_bounded_linear_map 𝕜 (λ x : E × F, x.1) :=
id               └───────────────────┘             
src              └───────────────────┘                 
typ              └───────────────────┘             
doc              └───────────────────┘
 63  begin
st   └─────
 64    refine (linear_map.fst 𝕜 E F).is_linear.with_bound 1 (λx, _),
id             └────────────┘   
src    └─────┘ └────────────┘   └───────────────────────┘  └───┘
typ    └─────┘ └────────────┘└───────────────────────┘  └───┘
doc    └─────┘ └────────────┘   └───────────────────────┘  └───┘
txt    └─────┘                  └───────────────────────┘  └───┘
par    └─────┘                  └───────────────────────┘  └───┘
pid                            └───────────────────────┘  └───┘
st   ─────────────────────────────────────────────────────────────┘└─
 65    rw one_mul,
id        └─────┘
src    └─┘└─────┘
typ    └─┘└─────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────┘└─
 66    exact le_max_left _ _
id           └─────────┘
src    └────┘└─────────┘└───┘
typ    └────┘└─────────┘└───┘
doc    └────┘           └───┘
txt    └────┘           └───┘
par    └────┘           └───┘
pid                    └──┘
st   ───────────────────────┘
 67  end
st   └─┘
 68  
 69  lemma snd : is_bounded_linear_map 𝕜 (λ x : E × F, x.2) :=
id               └───────────────────┘             
src              └───────────────────┘                 
typ              └───────────────────┘             
doc              └───────────────────┘
 70  begin
st   └─────
 71    refine (linear_map.snd 𝕜 E F).is_linear.with_bound 1 (λx, _),
id             └────────────┘   
src    └─────┘ └────────────┘   └───────────────────────┘  └───┘
typ    └─────┘ └────────────┘└───────────────────────┘  └───┘
doc    └─────┘ └────────────┘   └───────────────────────┘  └───┘
txt    └─────┘                  └───────────────────────┘  └───┘
par    └─────┘                  └───────────────────────┘  └───┘
pid                            └───────────────────────┘  └───┘
st   ─────────────────────────────────────────────────────────────┘└─
 72    rw one_mul,
id        └─────┘
src    └─┘└─────┘
typ    └─┘└─────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────┘└─
 73    exact le_max_right _ _
id           └──────────┘
src    └────┘└──────────┘└───┘
typ    └────┘└──────────┘└───┘
doc    └────┘            └───┘
txt    └────┘            └───┘
par    └────┘            └───┘
pid                     └──┘
st   ────────────────────────┘
 74  end
st   └─┘
 75  
 76  variables { f g : E → F }
 77  
 78  lemma smul (c : 𝕜) (hf : is_bounded_linear_map 𝕜 f) :
id                           └───────────────────┘  
src                           └───────────────────┘
typ                          └───────────────────┘  
doc                           └───────────────────┘
 79    is_bounded_linear_map 𝕜 (λ e, c • f e) :=
id     └───────────────────┘          
src    └───────────────────┘           
typ    └───────────────────┘          
doc    └───────────────────┘
 80  let ⟨hlf, M, hMp, hM⟩ := hf in
id   └─┘  └─┘         └┘     └┘
typ  └─┘  └─┘         └┘     └┘
 81  (c • hlf.mk' f).is_linear.with_bound (∥c∥ * M) $ assume x,
id         └──┘  └───────┘ └────────┘                 
src         └──┘   └───────┘ └────────┘     
typ        └──┘  └───────┘ └────────┘                 
 82    calc ∥c • f x∥ = ∥c∥ * ∥f x∥ : norm_smul c (f x)
id                      └───────┘    
src                           └───────┘
typ                     └───────┘    
 83    ... ≤ ∥c∥ * (M * ∥x∥)        : mul_le_mul_of_nonneg_left (hM _) (norm_nonneg _)
id                            └───────────────────────┘         └─────────┘
src                             └───────────────────────┘         └─────────┘
typ                           └───────────────────────┘         └─────────┘
 84    ... = (∥c∥ * M) * ∥x∥        : (mul_assoc _ _ _).symm
id                             └───────┘       └──┘
src                              └───────┘       └──┘
typ                            └───────┘       └──┘
 85  
 86  lemma neg (hf : is_bounded_linear_map 𝕜 f) :
id                   └───────────────────┘  
src                  └───────────────────┘
typ                  └───────────────────┘  
doc                  └───────────────────┘
 87    is_bounded_linear_map 𝕜 (λ e, -f e) :=
id     └───────────────────┘        
src    └───────────────────┘         
typ    └───────────────────┘        
doc    └───────────────────┘
 88  begin
st   └─────
 89    rw show (λ e, -f e) = (λ e, (-1 : 𝕜) • f e), { funext, simp },
id                                        
src    └─┘      └──┘  └┘  └──┘  └──┘ └┘  └───┘└────┘└┘└───┘
typ    └─┘      └──┘  └┘  └──┘  └──┘└┘ └───┘└────┘└┘└───┘
doc    └─┘      └──┘   └┘   └──┘  └──┘ └┘   └───┘└────┘└┘└───┘
txt    └─┘      └──┘   └┘   └──┘  └──┘ └┘   └───┘└────┘└┘└───┘
par    └─┘      └──┘   └┘   └──┘  └──┘ └┘   └───┘└────┘└┘└───┘
pid            └──┘   └┘   └──┘  └──┘ └┘   └─────────────────┘
st   ───────────────────────────────────────────────┘└─────┘└─────┘└┘
 90    exact smul (-1) hf
id           └──┘      └┘
src    └────┘└──┘  └─┘  
typ    └────┘└──┘  └─┘└┘
doc    └────┘      └─┘  
txt    └────┘      └─┘  
par    └────┘      └─┘  
pid               └─┘  
st   ────────────────────┘
 91  end
st   └─┘
 92  
 93  lemma add (hf : is_bounded_linear_map 𝕜 f) (hg : is_bounded_linear_map 𝕜 g) :
id                   └───────────────────┘          └───────────────────┘  
src                  └───────────────────┘            └───────────────────┘
typ                  └───────────────────┘          └───────────────────┘  
doc                  └───────────────────┘            └───────────────────┘
 94    is_bounded_linear_map 𝕜 (λ e, f e + g e) :=
id     └───────────────────┘           
src    └───────────────────┘             
typ    └───────────────────┘           
doc    └───────────────────┘
 95  let ⟨hlf, Mf, hMfp, hMf⟩ := hf in
id   └─┘  └─┘  └┘        └─┘     └┘
typ  └─┘  └─┘  └┘        └─┘     └┘
 96  let ⟨hlg, Mg, hMgp, hMg⟩ := hg in
id   └─┘  └─┘  └┘        └─┘     └┘
typ  └─┘  └─┘  └┘        └─┘     └┘
 97  (hlf.mk' _ + hlg.mk' _).is_linear.with_bound (Mf + Mg) $ assume x,
id       └──┘       └──┘   └───────┘ └────────┘                    
src      └──┘       └──┘   └───────┘ └────────┘      
typ      └──┘       └──┘   └───────┘ └────────┘                    
 98    calc ∥f x + g x∥ ≤ Mf * ∥x∥ + Mg * ∥x∥ : norm_add_le_of_le (hMf x) (hMg x)
id                              └───────────────┘             
src                                   └───────────────┘
typ                             └───────────────┘             
 99                 ... ≤ (Mf + Mg) * ∥x∥     : by rw add_mul
id                                               └─────┘
src                                            └─┘└─────┘
typ                                           └─┘└─────┘
doc                                                └─┘       
txt                                                └─┘       
par                                                └─┘       
pid                                                         
st                                                └───────────
100  
src  
typ  
doc  
txt  
par  
pid  
st   
101  lemma sub (hf : is_bounded_linear_map 𝕜 f) (hg : is_bounded_linear_map 𝕜 g) :
id                   └───────────────────┘          └───────────────────┘  
src                  └───────────────────┘            └───────────────────┘
typ                  └───────────────────┘          └───────────────────┘  
doc                  └───────────────────┘            └───────────────────┘
102    is_bounded_linear_map 𝕜 (λ e, f e - g e) := add hf (neg hg)
id     └───────────────────┘                └─┘ └┘  └─┘ └┘
src    └───────────────────┘                      └─┘     └─┘
typ    └───────────────────┘                └─┘ └┘  └─┘ └┘
doc    └───────────────────┘
103  
104  lemma comp {g : F → G}
id                      
typ                     
105    (hg : is_bounded_linear_map 𝕜 g) (hf : is_bounded_linear_map 𝕜 f) :
id           └───────────────────┘          └───────────────────┘  
src          └───────────────────┘            └───────────────────┘
typ          └───────────────────┘          └───────────────────┘  
doc          └───────────────────┘            └───────────────────┘
106    is_bounded_linear_map 𝕜 (g ∘ f) :=
id     └───────────────────┘     
src    └───────────────────┘      
typ    └───────────────────┘     
doc    └───────────────────┘
107  let ⟨hlg, Mg, hMgp, hMg⟩ := hg in
id   └─┘  └─┘  └┘  └──┘  └─┘     └┘
typ  └─┘  └─┘  └┘  └──┘  └─┘     └┘
108  let ⟨hlf, Mf, hMfp, hMf⟩ := hf in
id   └─┘  └─┘  └┘        └─┘     └┘
typ  └─┘  └─┘  └┘        └─┘     └┘
109  ((hlg.mk' _).comp (hlf.mk' _)).is_linear.with_bound (Mg * Mf) $ assume x,
id        └──┘   └──┘      └──┘    └───────┘ └────────┘                    
src       └──┘   └──┘      └──┘    └───────┘ └────────┘      
typ       └──┘   └──┘      └──┘    └───────┘ └────────┘                    
110    calc ∥g (f x)∥ ≤ Mg * ∥f x∥ : hMg _
id                      
src                          
typ                     
111      ... ≤ Mg * (Mf * ∥x∥) : mul_le_mul_of_nonneg_left (hMf _) (le_of_lt hMgp)
id                          └───────────────────────┘          └──────┘
src                          └───────────────────────┘          └──────┘
typ                         └───────────────────────┘          └──────┘
112      ... = Mg * Mf * ∥x∥   : (mul_assoc _ _ _).symm
id                           └───────┘       └──┘
src                           └───────┘       └──┘
typ                          └───────┘       └──┘
113  
114  lemma tendsto (x : E) (hf : is_bounded_linear_map 𝕜 f) : f →_{x} (f x) :=
id                              └───────────────────┘       └─┘   
src                              └───────────────────┘          └─┘ 
typ                             └───────────────────┘       └─┘   
doc                              └───────────────────┘          └─┘ 
115  let ⟨hf, M, hMp, hM⟩ := hf in
id   └─┘  └┘         └┘     └┘
typ  └─┘  └┘         └┘     └┘
116  tendsto_iff_norm_tendsto_zero.2 $
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
117    squeeze_zero (assume e, norm_nonneg _)
id     └──────────┘           └─────────┘
src    └──────────┘            └─────────┘
typ    └──────────┘           └─────────┘
118      (assume e,
id               
typ              
119        calc ∥f e - f x∥ = ∥hf.mk' f (e - x)∥ : by rw (hf.mk' _).map_sub e x; refl
id                       └──┘                └────┘             
src                          └──┘               └─┘ └────┘└──────────┘    └────
typ                      └──┘            └─┘ └────┘└──────────┘  └────
doc                                                   └─┘       └──────────┘    └────
txt                                                   └─┘       └──────────┘    └────
par                                                   └─┘       └──────────┘    └────
pid                                                            └──────────┘        
st                                                   └────────────────────────────────
120                     ... ≤ M * ∥e - x∥        : hM (e - x))
id                                                 
src  ──────────────────┘                             
typ  ──────────────────┘                           
doc  ──────────────────┘
txt  ──────────────────┘
par  ──────────────────┘
pid  ──────────────────┘
st   ──────────────────┘
121      (suffices (λ (e : E), M * ∥e - x∥) →_{x} (M * 0), by simpa,
id                                   └─┘    
src                                     └─┘             └───┘
typ                                  └─┘            └───┘
doc                                         └─┘              └───┘
txt                                                           └───┘
par                                                           └───┘
st                                                           └────┘
122        tendsto_const_nhds.mul (lim_norm _))
id         └────────────────┘└──┘  └──────┘
src        └────────────────┘└──┘  └──────┘
typ        └────────────────┘└──┘  └──────┘
123  
124  lemma continuous (hf : is_bounded_linear_map 𝕜 f) : continuous f :=
id                          └───────────────────┘      └────────┘ 
src                         └───────────────────┘        └────────┘
typ                         └───────────────────┘      └────────┘ 
doc                         └───────────────────┘        └────────┘
125  continuous_iff_continuous_at.2 $ λ _, hf.tendsto _
id   └──────────────────────────┘        └┘└──────┘
src  └──────────────────────────┘           └──────┘
typ  └──────────────────────────┘        └┘└──────┘
126  
127  lemma lim_zero_bounded_linear_map (hf : is_bounded_linear_map 𝕜 f) :
id                                           └───────────────────┘  
src                                          └───────────────────┘
typ                                          └───────────────────┘  
doc                                          └───────────────────┘
128    (f →_{0} 0) :=
id       └─┘ 
src       └─┘ 
typ      └─┘ 
doc       └─┘ 
129  (hf.1.mk' _).map_zero ▸ continuous_iff_continuous_at.1 hf.continuous 0
id    └┘ └─┘    └──────┘   └──────────────────────────┘  └┘└─────────┘
src      └─┘    └──────┘   └──────────────────────────┘    └─────────┘
typ   └┘ └─┘    └──────┘   └──────────────────────────┘  └┘└─────────┘
130  
131  section
132  open asymptotics filter
133  
134  theorem is_O_id {f : E → F} (h : is_bounded_linear_map 𝕜 f) (l : filter E) :
id                                  └───────────────────┘         └────┘ 
src                                   └───────────────────┘           └────┘
typ                                 └───────────────────┘         └────┘ 
doc                                   └───────────────────┘
135    is_O f (λ x, x) l :=
id     └──┘         
src    └──┘
typ    └──┘         
doc    └──┘
136  let ⟨M, hMp, hM⟩ := h.bound in
id   └─┘         └┘     └────┘
src                       └────┘
typ  └─┘         └┘     └────┘
137  ⟨M, mem_sets_of_superset univ_mem_sets (λ x _, hM x)⟩
id       └──────────────────┘ └───────────┘          
src      └──────────────────┘ └───────────┘
typ      └──────────────────┘ └───────────┘          
138  
139  theorem is_O_comp {E : Type*} {g : F → G} (hg : is_bounded_linear_map 𝕜 g)
id                                                 └───────────────────┘  
src                                                  └───────────────────┘
typ                                                └───────────────────┘  
doc                                                  └───────────────────┘
140    {f : E → F} (l : filter E) : is_O (λ x', g (f x')) f l :=
id                    └────┘     └──┘    └┘     └┘    
src                     └────┘      └──┘
typ                   └────┘     └──┘    └┘     └┘    
doc                                 └──┘
141  (hg.is_O_id ⊤).comp_tendsto lattice.le_top
id    └┘└──────┘  └──────────┘  └────────────┘
src     └──────┘  └──────────┘  └────────────┘
typ   └┘└──────┘  └──────────┘  └────────────┘
142  
143  theorem is_O_sub {f : E → F} (h : is_bounded_linear_map 𝕜 f)
id                                   └───────────────────┘  
src                                    └───────────────────┘
typ                                  └───────────────────┘  
doc                                    └───────────────────┘
144    (l : filter E) (x : E) : is_O (λ x', f (x' - x)) (λ x', x' - x) l :=
id          └────┘            └──┘    └┘    └┘        └┘  └┘    
src         └────┘              └──┘                             
typ         └────┘            └──┘    └┘    └┘        └┘  └┘    
doc                             └──┘
145  is_O_comp h l
id   └───────┘  
src  └───────┘
typ  └───────┘  
146  
147  end
148  
149  end is_bounded_linear_map
150  
151  section
152  set_option class.instance_max_depth 240
doc             └──────────────────────┘
153  
154  lemma is_bounded_linear_map_prod_iso :
155    is_bounded_linear_map 𝕜 (λ(p : (E →L[𝕜] F) × (E →L[𝕜] G)),
id     └───────────────────┘           └─┘      └─┘ 
src    └───────────────────┘             └─┘         └─┘ 
typ    └───────────────────┘           └─┘      └─┘ 
doc    └───────────────────┘             └─┘          └─┘ 
156                              (continuous_linear_map.prod p.1 p.2 : (E →L[𝕜] (F × G)))) :=
id                                └────────────────────────┘         └─┘    
src                               └────────────────────────┘            └─┘     
typ                               └────────────────────────┘         └─┘    
doc                               └────────────────────────┘              └─┘ 
157  begin
st   └─────
158    refine is_linear_map.with_bound ⟨λu v, rfl, λc u, rfl⟩ 1 (λp, _),
id            └──────────────────────┘                   └─┘
src    └─────┘└──────────────────────┘  └───┘   └┘ └───┘└─┘└──┘  └───┘
typ    └─────┘└──────────────────────┘  └───┘   └┘ └───┘└─┘└──┘  └───┘
doc    └─────┘                          └───┘   └┘ └───┘   └──┘  └───┘
txt    └─────┘                          └───┘   └┘ └───┘   └──┘  └───┘
par    └─────┘                          └───┘   └┘ └───┘   └──┘  └───┘
pid                                    └───┘   └┘ └───┘   └──┘  └───┘
st   ─────────────────────────────────────────────────────────────────┘└─
159    simp only [norm, one_mul],
id                      └─────┘
src    └─────────┘    └┘└─────┘
typ    └─────────┘    └┘└─────┘
doc    └─────────┘    └┘       
txt    └─────────┘    └┘       
par    └─────────┘    └┘       
pid        └──┘└┘    └┘       
st   ──────────────────────────┘└─
160    refine continuous_linear_map.op_norm_le_bound _ (le_trans (norm_nonneg _) (le_max_left _ _)) (λu, _),
id            └────────────────────────────────────┘    └──────┘  └─────────┘     └─────────┘
src    └─────┘└────────────────────────────────────┘└─┘ └──────┘ └─────────┘└──┘ └─────────┘└─────┘  └───┘
typ    └─────┘└────────────────────────────────────┘└─┘ └──────┘ └─────────┘└──┘ └─────────┘└─────┘  └───┘
doc    └─────┘└────────────────────────────────────┘└─┘                     └──┘            └─────┘  └───┘
txt    └─────┘                                      └─┘                     └──┘            └─────┘  └───┘
par    └─────┘                                      └─┘                     └──┘            └─────┘  └───┘
pid                                                └─┘                     └──┘            └─────┘  └───┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
161    simp only [norm, continuous_linear_map.prod, max_le_iff],
id                      └────────────────────────┘  └────────┘
src    └─────────┘    └┘└────────────────────────┘└┘└────────┘
typ    └─────────┘    └┘└────────────────────────┘└┘└────────┘
doc    └─────────┘    └┘└────────────────────────┘└┘          
txt    └─────────┘    └┘                          └┘          
par    └─────────┘    └┘                          └┘          
pid        └──┘└┘    └┘                          └┘          
st   ─────────────────────────────────────────────────────────┘└─
162    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
163    { calc ∥p.1 u∥ ≤ ∥p.1∥ * ∥u∥ : continuous_linear_map.le_op_norm _ _
id       └──┘                       └──────────────────────────────┘
src      └──┘                       └──────────────────────────────┘
typ      └──┘                       └──────────────────────────────┘
doc      └──┘                         └──────────────────────────────┘
st   ───┘└─────────────────────────────────────────────────────────────────
164      ... ≤ max (∥p.1∥) (∥p.2∥) * ∥u∥ :
id             └─┘                  
src            └─┘            
typ            └─┘                  
st   ──────────────────────────────────────
165        mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) },
id         └────────────────────────┘  └─────────┘       └─────────┘
src        └────────────────────────┘  └─────────┘       └─────────┘
typ        └────────────────────────┘  └─────────┘       └─────────┘
st   ─────────────────────────────────────────────────────────────────┘└─┘
166    { calc ∥p.2 u∥ ≤ ∥p.2∥ * ∥u∥ : continuous_linear_map.le_op_norm _ _
id       └──┘                         └──────────────────────────────┘
src      └──┘                         └──────────────────────────────┘
typ      └──┘                         └──────────────────────────────┘
doc      └──┘                         └──────────────────────────────┘
st   ──────────────────────────────────────────────────────────────────────
167      ... ≤ max (∥p.1∥) (∥p.2∥) * ∥u∥ :
id             └─┘                   
src            └─┘
typ            └─┘                   
st   ──────────────────────────────────────
168        mul_le_mul_of_nonneg_right (le_max_right _ _) (norm_nonneg _) }
id         └────────────────────────┘  └──────────┘       └─────────┘
src        └────────────────────────┘  └──────────┘       └─────────┘
typ        └────────────────────────┘  └──────────┘       └─────────┘
st   ──────────────────────────────────────────────────────────────────┘└──
169  end
st   ──┘
170  
171  lemma continuous_linear_map.is_bounded_linear_map_comp_left (g : continuous_linear_map 𝕜 F G) :
id                                                                    └───────────────────┘   
src                                                                   └───────────────────┘
typ                                                                   └───────────────────┘   
doc                                                                   └───────────────────┘
172    is_bounded_linear_map 𝕜 (λ(f : E →L[𝕜] F), continuous_linear_map.comp g f) :=
id     └───────────────────┘          └─┘    └────────────────────────┘  
src    └───────────────────┘            └─┘      └────────────────────────┘
typ    └───────────────────┘          └─┘    └────────────────────────┘  
doc    └───────────────────┘            └─┘      └────────────────────────┘
173  begin
st   └─────
174    refine is_linear_map.with_bound ⟨λu v, _, λc u, _⟩
id            └──────────────────────┘
src    └─────┘└──────────────────────┘  └──────┘ └───────
typ    └─────┘└──────────────────────┘  └──────┘ └───────
doc    └─────┘                          └──────┘ └───────
txt    └─────┘                          └──────┘ └───────
par    └─────┘                          └──────┘ └───────
pid                                    └──────┘ └───────
st   ─────────────────────────────────────────────────────
175      (∥g∥) (λu, continuous_linear_map.op_norm_comp_le _ _),
id               └───────────────────────────────────┘
src  ───┘  └┘  └─┘└───────────────────────────────────┘└───┘
typ  ───┘ └┘  └─┘└───────────────────────────────────┘└───┘
doc  ───┘    └┘  └─┘└───────────────────────────────────┘└───┘
txt  ───┘    └┘  └─┘                                     └───┘
par  ───┘    └┘  └─┘                                     └───┘
pid  ───┘    └┘  └─┘                                     └───┘
st   ────────────────────────────────────────────────────────┘└─
176    { ext x,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
177      change g ((u+v) x) = g (u x) + g (v x),
id                                      
src      └─────┘     └┘ └┘    └┘     
typ      └─────┘     └┘ └┘   └┘  
doc      └─────┘      └┘ └┘     └┘     
txt      └─────┘      └┘ └┘     └┘     
par      └─────┘      └┘ └┘     └┘     
pid                  └┘ └┘     └┘     
st   ─────────────────────────────────────────┘└─
178      have : (u+v) x = u x + v x := rfl,
id                                  └─┘
src      └─────┘    └┘       └──┘└─┘
typ      └─────┘    └┘    └──┘└─┘
doc      └─────┘    └┘       └──┘
txt      └─────┘    └┘       └──┘
par      └─────┘    └┘       └──┘
pid      └───┘└┘    └┘       └──┘
st   ────────────────────────────────────┘└─
179      rw [this, g.map_add] },
id           └──┘
src      └──┘    └┘         └┘
typ      └──┘└──┘└┘└───────┘└┘
doc      └──┘    └┘         └┘
txt      └──┘    └┘         └┘
par      └──┘    └┘         └┘
pid        └┘    └┘         
st   ───────────┘└─────────┘└┘
180    { ext x,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ────────┘└─
181      change g ((c • u) x) = c • g (u x),
id                                   
src      └─────┘     └┘ └┘       
typ      └─────┘     └┘ └┘   
doc      └─────┘      └┘ └┘       
txt      └─────┘      └┘ └┘       
par      └─────┘      └┘ └┘       
pid                  └┘ └┘       
st   ─────────────────────────────────────┘└─
182      have : (c • u) x = c • u x := rfl,
id                                  └─┘
src      └─────┘    └┘      └──┘└─┘
typ      └─────┘    └┘   └──┘└─┘
doc      └─────┘    └┘      └──┘
txt      └─────┘    └┘      └──┘
par      └─────┘    └┘      └──┘
pid      └───┘└┘    └┘      └──┘
st   ────────────────────────────────────┘└─
183      rw [this, continuous_linear_map.map_smul] }
id           └──┘  └────────────────────────────┘
src      └──┘    └┘└────────────────────────────┘└┘
typ      └──┘└──┘└┘└────────────────────────────┘└┘
doc      └──┘    └┘                              └┘
txt      └──┘    └┘                              └┘
par      └──┘    └┘                              └┘
pid        └┘    └┘                              
st   ───────────┘└──────────────────────────────┘└─
184  end
st   ──┘
185  
186  lemma continuous_linear_map.is_bounded_linear_map_comp_right (f : continuous_linear_map 𝕜 E F) :
id                                                                     └───────────────────┘   
src                                                                    └───────────────────┘
typ                                                                    └───────────────────┘   
doc                                                                    └───────────────────┘
187    is_bounded_linear_map 𝕜 (λ(g : F →L[𝕜] G), continuous_linear_map.comp g f) :=
id     └───────────────────┘          └─┘    └────────────────────────┘  
src    └───────────────────┘            └─┘      └────────────────────────┘
typ    └───────────────────┘          └─┘    └────────────────────────┘  
doc    └───────────────────┘            └─┘      └────────────────────────┘
188  begin
st   └─────
189    refine is_linear_map.with_bound ⟨λu v, rfl, λc u, rfl⟩ (∥f∥) (λg, _),
id            └──────────────────────┘                   └─┘   
src    └─────┘└──────────────────────┘  └───┘   └┘ └───┘└─┘└┘  └┘  └───┘
typ    └─────┘└──────────────────────┘  └───┘   └┘ └───┘└─┘└┘ └┘  └───┘
doc    └─────┘                          └───┘   └┘ └───┘   └┘    └┘  └───┘
txt    └─────┘                          └───┘   └┘ └───┘   └┘    └┘  └───┘
par    └─────┘                          └───┘   └┘ └───┘   └┘    └┘  └───┘
pid                                    └───┘   └┘ └───┘   └┘    └┘  └───┘
st   ─────────────────────────────────────────────────────────────────────┘└─
190    rw mul_comm,
id        └──────┘
src    └─┘└──────┘
typ    └─┘└──────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────┘└─
191    exact continuous_linear_map.op_norm_comp_le _ _
id           └───────────────────────────────────┘
src    └────┘└───────────────────────────────────┘└───┘
typ    └────┘└───────────────────────────────────┘└───┘
doc    └────┘└───────────────────────────────────┘└───┘
txt    └────┘                                     └───┘
par    └────┘                                     └───┘
pid                                              └──┘
st   ─────────────────────────────────────────────────┘
192  end
st   └─┘
193  
194  end
195  
196  section bilinear_map
197  
198  variable (𝕜)
199  
200  /-- A map `f : E × F → G` satisfies `is_bounded_bilinear_map 𝕜 f` if it is bilinear and
201  continuous. -/
202  structure is_bounded_bilinear_map (f : E × F → G) : Prop :=
id                                              
src                                           
typ                                             
203  (add_left   : ∀(x₁ x₂ : E) (y : F), f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y))
id                                     └┘  └┘      └┘      └┘  
src                                                                
typ                                    └┘  └┘      └┘      └┘  
204  (smul_left  : ∀(c : 𝕜) (x : E) (y : F), f (c • x, y) = c • f (x,y))
id                                                   
src                                                           
typ                                                  
205  (add_right  : ∀(x : E) (y₁ y₂ : F), f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂))
id                                       └┘  └┘      └┘      └┘
src                                                                
typ                                      └┘  └┘      └┘      └┘
206  (smul_right : ∀(c : 𝕜) (x : E) (y : F), f (x, c • y) = c • f (x,y))
id                                                   
src                                                           
typ                                                  
207  (bound      : ∃C>0, ∀(x : E) (y : F), ∥f (x, y)∥ ≤ C * ∥x∥ * ∥y∥)
id                                              
src                                                      
typ                                             
208  
209  variable {𝕜}
210  variable {f : E × F → G}
id                   
src                  
typ                  
211  
212  lemma is_bounded_bilinear_map.map_sub_left (h : is_bounded_bilinear_map 𝕜 f) {x y : E} {z : F} :
id                                                   └─────────────────────┘                  
src                                                  └─────────────────────┘
typ                                                  └─────────────────────┘                  
doc                                                  └─────────────────────┘
213    f (x - y, z) = f (x, z) -  f(y, z) :=
id                      
src                           
typ                     
214  calc f (x - y, z) = f (x + (-1 : 𝕜) • y, z) : by simp
id                              
src                                             └───┘
typ                                    └───┘
doc                                                   └───┘
txt                                                   └───┘
par                                                   └───┘
pid                                                       
st                                                   └────┘
215  ... = f (x, z) + (-1 : 𝕜) • f (y, z) : by simp only [h.add_left, h.smul_left]
id                          
src                                       └─────────┘          └┘           └┘
typ                                └─────────┘└────────┘└┘└─────────┘└┘
doc                                            └─────────┘          └┘           └┘
txt                                            └─────────┘          └┘           └┘
par                                            └─────────┘          └┘           └┘
pid                                                └──┘└┘          └┘           
st                                            └───────────────────────────────────┘
216  ... = f (x, z) - f (y, z) : by simp
id                  
src                              └────
typ                        └────
doc                                 └────
txt                                 └────
par                                 └────
pid                                     
st                                 └─────
217  
src  
typ  
doc  
txt  
par  
pid  
st   
218  lemma is_bounded_bilinear_map.map_sub_right (h : is_bounded_bilinear_map 𝕜 f) {x : E} {y z : F} :
id                                                    └─────────────────────┘                  
src                                                   └─────────────────────┘
typ                                                   └─────────────────────┘                  
doc                                                   └─────────────────────┘
219    f (x, y - z) = f (x, y) - f (x, z) :=
id                      
src                           
typ                     
220  calc f (x, y - z) = f (x, y + (-1 : 𝕜) • z) : by simp
id                              
src                                             └───┘
typ                                    └───┘
doc                                                   └───┘
txt                                                   └───┘
par                                                   └───┘
pid                                                       
st                                                   └────┘
221  ... = f (x, y) + (-1 : 𝕜) • f (x, z) : by simp only [h.add_right, h.smul_right]
id                          
src                                       └─────────┘           └┘            └┘
typ                                └─────────┘└─────────┘└┘└──────────┘└┘
doc                                            └─────────┘           └┘            └┘
txt                                            └─────────┘           └┘            └┘
par                                            └─────────┘           └┘            └┘
pid                                                └──┘└┘           └┘            
st                                            └─────────────────────────────────────┘
222  ... = f (x, y) - f (x, z) : by simp
id                  
src                              └────
typ                        └────
doc                                 └────
txt                                 └────
par                                 └────
pid                                     
st                                 └─────
223  
src  
typ  
doc  
txt  
par  
pid  
st   
224  lemma is_bounded_bilinear_map_smul :
225    is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × E), p.1 • p.2) :=
id     └─────────────────────┘                  
src    └─────────────────────┘                       
typ    └─────────────────────┘                  
doc    └─────────────────────┘
226  { add_left   := add_smul,
id                   └──────┘
src                  └──────┘
typ                  └──────┘
227    smul_left  := λc x y, by simp [smul_smul],
id                                 └───────┘
src                             └────┘└───────┘
typ                          └────┘└───────┘
doc                             └────┘         
txt                             └────┘         
par                             └────┘         
pid                                          
st                             └───────────────┘
228    add_right  := smul_add,
id                   └──────┘
src                  └──────┘
typ                  └──────┘
229    smul_right := λc x y, by simp [smul_smul, mul_comm],
id                                 └───────┘  └──────┘
src                             └────┘└───────┘└┘└──────┘
typ                          └────┘└───────┘└┘└──────┘
doc                             └────┘         └┘        
txt                             └────┘         └┘        
par                             └────┘         └┘        
pid                                          └┘        
st                             └─────────────────────────┘
230    bound      := ⟨1, zero_lt_one, λx y, by simp [norm_smul]⟩ }
id                       └─────────┘               └───────┘
src                      └─────────┘           └────┘└───────┘
typ                      └─────────┘         └────┘└───────┘
doc                                            └────┘         
txt                                            └────┘         
par                                            └────┘         
pid                                                         
st                                            └───────────────┘
231  
232  lemma is_bounded_bilinear_map_mul :
233    is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × 𝕜), p.1 * p.2) :=
id     └─────────────────────┘                  
src    └─────────────────────┘                       
typ    └─────────────────────┘                  
doc    └─────────────────────┘
234  is_bounded_bilinear_map_smul
id   └──────────────────────────┘
src  └──────────────────────────┘
typ  └──────────────────────────┘
235  
236  lemma is_bounded_bilinear_map_comp :
237    is_bounded_bilinear_map 𝕜 (λ(p : (E →L[𝕜] F) × (F →L[𝕜] G)), p.2.comp p.1) :=
id     └─────────────────────┘           └─┘      └─┘      └──┘  
src    └─────────────────────┘             └─┘         └─┘         └──┘   
typ    └─────────────────────┘           └─┘      └─┘      └──┘  
doc    └─────────────────────┘             └─┘          └─┘          └──┘
238  { add_left := λx₁ x₂ y, begin
id                  └┘ └┘ 
typ                 └┘ └┘ 
st                           └─────
239        ext z,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid           └┘
st   ──────────┘└─
240        change y (x₁ z + x₂ z) = y (x₁ z) + y (x₂ z),
id                                   └┘        └┘ 
src        └─────┘        └┘     └┘      
typ        └─────┘        └┘  └┘ └┘  └┘
doc        └─────┘         └┘      └┘      
txt        └─────┘         └┘      └┘      
par        └─────┘         └┘      └┘      
pid                       └┘      └┘      
st   ─────────────────────────────────────────────────┘└─
241        rw y.map_add
src        └─┘         
typ        └─┘└───────┘
doc        └─┘         
txt        └─┘         
par        └─┘         
pid                   
st   ───────────────────
242      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
243    smul_left := λc x y, begin
id                     
typ                    
st                          └─────
244        ext z,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid           └┘
st   ──────────┘└─
245        change y (c • (x z)) = c • y (x z),
id                                     
src        └─────┘      └─┘       
typ        └─────┘      └─┘   
doc        └─────┘       └─┘       
txt        └─────┘       └─┘       
par        └─────┘       └─┘       
pid                     └─┘       
st   ───────────────────────────────────────┘└─
246        rw continuous_linear_map.map_smul
id            └────────────────────────────┘
src        └─┘└────────────────────────────┘
typ        └─┘└────────────────────────────┘
doc        └─┘                              
txt        └─┘                              
par        └─┘                              
pid                                        
st   ────────────────────────────────────────
247      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
248    add_right := λx y₁ y₂, rfl,
id                    └┘ └┘  └─┘
src                           └─┘
typ                   └┘ └┘  └─┘
249    smul_right := λc x y, rfl,
id                        └─┘
src                          └─┘
typ                       └─┘
250    bound := ⟨1, zero_lt_one, λx y, calc
id                  └─────────┘    
src                 └─────────┘
typ                 └─────────┘    
251      ∥continuous_linear_map.comp ((x, y).snd) ((x, y).fst)∥
id       └────────────────────────┘     └─┘       └─┘  
src      └────────────────────────┘       └─┘         └─┘  
typ      └────────────────────────┘     └─┘       └─┘  
doc       └────────────────────────┘
252        ≤ ∥y∥ * ∥x∥ : continuous_linear_map.op_norm_comp_le _ _
id                └───────────────────────────────────┘
src                 └───────────────────────────────────┘
typ               └───────────────────────────────────┘
doc                      └───────────────────────────────────┘
253      ... = 1 * ∥x∥ * ∥ y∥ : by ring ⟩ }
id                   
src                          └───┘
typ                        └───┘
doc                                └───┘
txt                                └───┘
par                                └───┘
pid                                    
st                                └────┘
254  
255  lemma is_bounded_bilinear_map_apply :
256    is_bounded_bilinear_map 𝕜 (λp : (E →L[𝕜] F) × E, p.1 p.2) :=
id     └─────────────────────┘          └─┘        
src    └─────────────────────┘            └─┘             
typ    └─────────────────────┘          └─┘        
doc    └─────────────────────┘            └─┘ 
257  { add_left   := by simp,
src                     └──┘
typ                     └──┘
doc                     └──┘
txt                     └──┘
par                     └──┘
st                     └───┘
258    smul_left  := by simp,
src                     └──┘
typ                     └──┘
doc                     └──┘
txt                     └──┘
par                     └──┘
st                     └───┘
259    add_right  := by simp,
src                     └──┘
typ                     └──┘
doc                     └──┘
txt                     └──┘
par                     └──┘
st                     └───┘
260    smul_right := by simp,
src                     └──┘
typ                     └──┘
doc                     └──┘
txt                     └──┘
par                     └──┘
st                     └───┘
261    bound      := ⟨1, zero_lt_one, by simp [continuous_linear_map.le_op_norm]⟩ }
id                       └─────────┘           └──────────────────────────────┘
src                      └─────────┘     └────┘└──────────────────────────────┘
typ                      └─────────┘     └────┘└──────────────────────────────┘
doc                                      └────┘└──────────────────────────────┘
txt                                      └────┘                                
par                                      └────┘                                
pid                                                                          
st                                      └──────────────────────────────────────┘
262  
263  /-- The function `continuous_linear_map.smul_right`, associating to a continuous linear map
264  `f : E → 𝕜` and a scalar `c : F` the tensor product `f ⊗ c` as a continuous linear map from `E` to
265  `F`, is a bounded bilinear map. -/
266  lemma is_bounded_bilinear_map_smul_right :
267    is_bounded_bilinear_map 𝕜
id     └─────────────────────┘ 
src    └─────────────────────┘
typ    └─────────────────────┘ 
doc    └─────────────────────┘
268      (λp, (continuous_linear_map.smul_right : (E →L[𝕜] 𝕜) → F → (E →L[𝕜] F)) p.1 p.2) :=
id            └──────────────────────────────┘     └─┘          └─┘      
src            └──────────────────────────────┘      └─┘              └─┘          
typ           └──────────────────────────────┘     └─┘          └─┘      
doc            └──────────────────────────────┘      └─┘              └─┘ 
269  { add_left   := λm₁ m₂ f, by { ext z, simp [add_smul] },
id                    └┘ └┘                     └──────┘
src                                 └───┘  └────┘└──────┘└┘
typ                   └┘ └┘        └───┘  └────┘└──────┘└┘
doc                                 └───┘  └────┘        └┘
txt                                 └───┘  └────┘        └┘
par                                 └───┘  └────┘        └┘
pid                                    └┘              
st                               └──────┘└────────────────┘└┘
270    smul_left  := λc m f, by { ext z, simp [mul_smul] },
id                                          └──────┘
src                               └───┘  └────┘└──────┘└┘
typ                            └───┘  └────┘└──────┘└┘
doc                               └───┘  └────┘        └┘
txt                               └───┘  └────┘        └┘
par                               └───┘  └────┘        └┘
pid                                  └┘              
st                             └──────┘└────────────────┘└┘
271    add_right  := λm f₁ f₂, by { ext z, simp [smul_add] },
id                     └┘ └┘                    └──────┘
src                                 └───┘  └────┘└──────┘└┘
typ                    └┘ └┘       └───┘  └────┘└──────┘└┘
doc                                 └───┘  └────┘        └┘
txt                                 └───┘  └────┘        └┘
par                                 └───┘  └────┘        └┘
pid                                    └┘              
st                               └──────┘└────────────────┘└┘
272    smul_right := λc m f, by { ext z, simp [smul_smul, mul_comm] },
id                                          └───────┘  └──────┘
src                               └───┘  └────┘└───────┘└┘└──────┘└┘
typ                            └───┘  └────┘└───────┘└┘└──────┘└┘
doc                               └───┘  └────┘         └┘        └┘
txt                               └───┘  └────┘         └┘        └┘
par                               └───┘  └────┘         └┘        └┘
pid                                  └┘               └┘        
st                             └──────┘└───────────────────────────┘└┘
273    bound      := ⟨1, zero_lt_one, λm f, by simp⟩ }
id                       └─────────┘    
src                      └─────────┘           └──┘
typ                      └─────────┘         └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
274  
275  /-- Definition of the derivative of a bilinear map `f`, given at a point `p` by
276  `q ↦ f(p.1, q.2) + f(q.1, p.2)` as in the standard formula for the derivative of a product.
277  We define this function here a bounded linear map from `E × F` to `G`. The fact that this
278  is indeed the derivative of `f` is proved in `is_bounded_bilinear_map.has_fderiv_at` in
279  `fderiv.lean`-/
280  
281  def is_bounded_bilinear_map.linear_deriv (h : is_bounded_bilinear_map 𝕜 f) (p : E × F) :
id                                                 └─────────────────────┘           
src                                                └─────────────────────┘             
typ                                                └─────────────────────┘           
doc                                                └─────────────────────┘
282    (E × F) →ₗ[𝕜] G :=
id          └─┘ 
src           └─┘ 
typ         └─┘ 
283  { to_fun := λq, f (p.1, q.2) + f (q.1, p.2),
id                              
src                                    
typ                             
284    add := λq₁ q₂, begin
id             └┘ └┘
typ            └┘ └┘
st                    └─────
285      change f (p.1, q₁.2 + q₂.2) + f (q₁.1 + q₂.1, p.2) =
id                                                         
src      └─────┘   └──┘  └─┘  └──┘     └─┘   └──┘ └──┘
typ      └─────┘   └──┘  └─┘  └──┘     └─┘   └──┘ └──┘
doc      └─────┘   └──┘  └─┘   └──┘     └─┘   └──┘ └──┘ 
txt      └─────┘   └──┘  └─┘   └──┘     └─┘   └──┘ └──┘ 
par      └─────┘   └──┘  └─┘   └──┘     └─┘   └──┘ └──┘ 
pid               └──┘  └─┘   └──┘     └─┘   └──┘ └──┘ 
st   ─────────────────────────────────────────────────────────
286        f (p.1, q₁.2) + f (q₁.1, p.2) + (f (p.1, q₂.2) + f (q₂.1, p.2)),
id                            └┘                             └┘    
src  ─────┘   └──┘  └──┘     └──┘ └──┘     └──┘  └──┘    └──┘ └──┘
typ  ─────┘   └──┘  └──┘   └┘└──┘ └──┘     └──┘  └──┘ └┘└──┘└──┘
doc  ─────┘   └──┘  └──┘     └──┘ └──┘     └──┘  └──┘     └──┘ └──┘
txt  ─────┘   └──┘  └──┘     └──┘ └──┘     └──┘  └──┘     └──┘ └──┘
par  ─────┘   └──┘  └──┘     └──┘ └──┘     └──┘  └──┘     └──┘ └──┘
pid  ─────┘   └──┘  └──┘     └──┘ └──┘     └──┘  └──┘     └──┘ └──┘
st   ────────────────────────────────────────────────────────────────────┘└─
287      simp [h.add_left, h.add_right]
src      └────┘          └┘           └─
typ      └────┘└────────┘└┘└─────────┘└─
doc      └────┘          └┘           └─
txt      └────┘          └┘           └─
par      └────┘          └┘           └─
pid                    └┘           
st   ───────────────────────────────────
288    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
289    smul := λc q, begin
id               
typ              
st                   └─────
290      change f (p.1, c • q.2) + f (c • q.1, p.2) = c • (f (p.1, q.2) + f (q.1, p.2)),
id                                                                           
src      └─────┘   └──┘  └──┘      └──┘ └──┘       └──┘ └──┘   └──┘ └──┘
typ      └─────┘   └──┘  └──┘      └──┘ └──┘      └──┘ └──┘ └──┘└──┘
doc      └─────┘   └──┘   └──┘      └──┘ └──┘       └──┘ └──┘    └──┘ └──┘
txt      └─────┘   └──┘   └──┘      └──┘ └──┘       └──┘ └──┘    └──┘ └──┘
par      └─────┘   └──┘   └──┘      └──┘ └──┘       └──┘ └──┘    └──┘ └──┘
pid               └──┘   └──┘      └──┘ └──┘       └──┘ └──┘    └──┘ └──┘
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
291      simp [h.smul_left, h.smul_right, smul_add]
id                                        └──────┘
src      └────┘           └┘            └┘└──────┘└─
typ      └────┘└─────────┘└┘└──────────┘└┘└──────┘└─
doc      └────┘           └┘            └┘        └─
txt      └────┘           └┘            └┘        └─
par      └────┘           └┘            └┘        └─
pid                     └┘            └┘        
st   ───────────────────────────────────────────────
292    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
293  
294  /-- The derivative of a bounded bilinear map at a point `p : E × F`, as a continuous linear map
295  from `E × F` to `G`. -/
296  def is_bounded_bilinear_map.deriv (h : is_bounded_bilinear_map 𝕜 f) (p : E × F) : (E × F) →L[𝕜] G :=
id                                          └─────────────────────┘                    └─┘ 
src                                         └─────────────────────┘                          └─┘ 
typ                                         └─────────────────────┘                    └─┘ 
doc                                         └─────────────────────┘                            └─┘ 
297  (h.linear_deriv p).mk_continuous_of_exists_bound $ begin
id    └───────────┘  └───────────────────────────┘
src    └───────────┘   └───────────────────────────┘
typ   └───────────┘  └───────────────────────────┘
doc    └───────────┘   └───────────────────────────┘
st                                                      └─────
298    rcases h.bound with ⟨C, Cpos, hC⟩,
id            └─────┘
src    └─────┘└─────┘└─────────────────┘
typ    └─────┘└─────┘└─────────────────┘
doc    └─────┘       └─────────────────┘
txt    └─────┘       └─────────────────┘
par    └─────┘       └─────────────────┘
pid                 └─────────────────┘
st   ──────────────────────────────────┘└─
299    refine ⟨C * ∥p.1∥ + C * ∥p.2∥, λq, _⟩,
id                         
src    └─────┘   └┘    └┘ └┘ └───┘
typ    └─────┘   └┘  └┘ └┘ └───┘
doc    └─────┘     └┘      └┘ └┘ └───┘
txt    └─────┘     └┘      └┘ └┘ └───┘
par    └─────┘     └┘      └┘ └┘ └───┘
pid               └┘      └┘ └┘ └───┘
st   ──────────────────────────────────────┘└─
300    calc ∥f (p.1, q.2) + f (q.1, p.2)∥
id     └──┘                   
src    └──┘                    
typ    └──┘                   
doc    └──┘
st   ─────────────────────────────────────
301      ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : norm_add_le_of_le (hC _ _) (hC _ _)
id                                              └───────────────┘           └┘
src                                                └───────────────┘
typ                                             └───────────────┘           └┘
st   ──────────────────────────────────────────────────────────────────────────────────
302    ... ≤ C * ∥p.1∥ * ∥q∥ + C * ∥q∥ * ∥p.2∥ : begin
st   ───────────────────────────────────────────┘└─────
303        apply add_le_add,
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────┘└─
304        exact mul_le_mul_of_nonneg_left (le_max_right _ _) (mul_nonneg (le_of_lt Cpos) (norm_nonneg _)),
id               └───────────────────────┘  └──────────┘       └────────┘  └──────┘ └──┘   └─────────┘
src        └────┘└───────────────────────┘ └──────────┘└────┘ └────────┘ └──────┘    └┘ └─────────┘└──┘
typ        └────┘└───────────────────────┘ └──────────┘└────┘ └────────┘ └──────┘└──┘└┘ └─────────┘└──┘
doc        └────┘                                      └────┘                        └┘            └──┘
txt        └────┘                                      └────┘                        └┘            └──┘
par        └────┘                                      └────┘                        └┘            └──┘
pid                                                   └────┘                        └┘            └──┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
305        apply mul_le_mul_of_nonneg_right _ (norm_nonneg _),
id               └────────────────────────┘    └─────────┘
src        └────┘└────────────────────────┘└─┘ └─────────┘└─┘
typ        └────┘└────────────────────────┘└─┘ └─────────┘└─┘
doc        └────┘                          └─┘            └─┘
txt        └────┘                          └─┘            └─┘
par        └────┘                          └─┘            └─┘
pid                                       └─┘            └─┘
st   ───────────────────────────────────────────────────────┘└─
306        exact mul_le_mul_of_nonneg_left (le_max_left _ _) (le_of_lt Cpos),
id               └───────────────────────┘  └─────────┘       └──────┘ └──┘
src        └────┘└───────────────────────┘ └─────────┘└────┘ └──────┘    
typ        └────┘└───────────────────────┘ └─────────┘└────┘ └──────┘└──┘
doc        └────┘                                     └────┘             
txt        └────┘                                     └────┘             
par        └────┘                                     └────┘             
pid                                                  └────┘             
st   ──────────────────────────────────────────────────────────────────────┘└─
307    end
st   ────┘
308    ... = (C * ∥p.1∥ + C * ∥p.2∥) * ∥q∥ : by ring
src                                             └───┘
typ                                             └───┘
doc                                             └───┘
txt                                             └───┘
par                                             └───┘
pid                                                 
st   ─────────────────────────────────────────┘└────┘
309  end
st   └─┘
310  
311  @[simp] lemma is_bounded_bilinear_map_deriv_coe (h : is_bounded_bilinear_map 𝕜 f) (p q : E × F) :
id                                                        └─────────────────────┘             
src                                                       └─────────────────────┘               
typ                                                       └─────────────────────┘             
doc    └──┘                                               └─────────────────────┘
312    h.deriv p q = f (p.1, q.2) + f (q.1, p.2) := rfl
id     └────┘                      └─┘
src     └────┘                              └─┘
typ    └────┘                      └─┘
doc     └────┘
313  
314  set_option class.instance_max_depth 100
doc             └──────────────────────┘
315  
316  /-- Given a bounded bilinear map `f`, the map associating to a point `p` the derivative of `f` at
317  `p` is itself a bounded linear map. -/
318  lemma is_bounded_bilinear_map.is_bounded_linear_map_deriv (h : is_bounded_bilinear_map 𝕜 f) :
id                                                                  └─────────────────────┘  
src                                                                 └─────────────────────┘
typ                                                                 └─────────────────────┘  
doc                                                                 └─────────────────────┘
319    is_bounded_linear_map 𝕜 (λp : E × F, h.deriv p) :=
id     └───────────────────┘            └────┘ 
src    └───────────────────┘                └────┘
typ    └───────────────────┘            └────┘ 
doc    └───────────────────┘                 └────┘
320  begin
st   └─────
321    rcases h.bound with ⟨C, Cpos, hC⟩,
id            └─────┘
src    └─────┘└─────┘└─────────────────┘
typ    └─────┘└─────┘└─────────────────┘
doc    └─────┘       └─────────────────┘
txt    └─────┘       └─────────────────┘
par    └─────┘       └─────────────────┘
pid                 └─────────────────┘
st   ──────────────────────────────────┘└─
322    refine is_linear_map.with_bound ⟨λp₁ p₂, _, λc p, _⟩ (C + C) (λp, _),
id            └──────────────────────┘                          
src    └─────┘└──────────────────────┘  └────────┘ └──────┘   └┘  └───┘
typ    └─────┘└──────────────────────┘  └────────┘ └──────┘  └┘  └───┘
doc    └─────┘                          └────────┘ └──────┘    └┘  └───┘
txt    └─────┘                          └────────┘ └──────┘    └┘  └───┘
par    └─────┘                          └────────┘ └──────┘    └┘  └───┘
pid                                    └────────┘ └──────┘    └┘  └───┘
st   ─────────────────────────────────────────────────────────────────────┘└─
323    { ext q,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
324      simp [h.add_left, h.add_right] },
src      └────┘          └┘           └┘
typ      └────┘└────────┘└┘└─────────┘└┘
doc      └────┘          └┘           └┘
txt      └────┘          └┘           └┘
par      └────┘          └┘           └┘
pid                    └┘           
st   ──────────────────────────────────┘└┘
325    { ext q,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
326      simp [h.smul_left, h.smul_right, smul_add] },
id                                        └──────┘
src      └────┘           └┘            └┘└──────┘└┘
typ      └────┘└─────────┘└┘└──────────┘└┘└──────┘└┘
doc      └────┘           └┘            └┘        └┘
txt      └────┘           └┘            └┘        └┘
par      └────┘           └┘            └┘        └┘
pid                     └┘            └┘        
st   ──────────────────────────────────────────────┘└┘
327    { refine continuous_linear_map.op_norm_le_bound _
id              └────────────────────────────────────┘
src      └─────┘└────────────────────────────────────┘└──
typ      └─────┘└────────────────────────────────────┘└──
doc      └─────┘└────────────────────────────────────┘└──
txt      └─────┘                                      └──
par      └─────┘                                      └──
pid                                                  └──
st   ────────────────────────────────────────────────────
328        (mul_nonneg (add_nonneg (le_of_lt Cpos) (le_of_lt Cpos)) (norm_nonneg _)) (λq, _),
id          └────────┘  └────────┘                  └──────┘ └──┘    └─────────┘
src  ─────┘ └────────┘ └────────┘             └┘ └──────┘    └─┘ └─────────┘└───┘  └───┘
typ  ─────┘ └────────┘ └────────┘             └┘ └──────┘└──┘└─┘ └─────────┘└───┘  └───┘
doc  ─────┘                                   └┘             └─┘            └───┘  └───┘
txt  ─────┘                                   └┘             └─┘            └───┘  └───┘
par  ─────┘                                   └┘             └─┘            └───┘  └───┘
pid  ─────┘                                   └┘             └─┘            └───┘  └───┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
329      calc ∥f (p.1, q.2) + f (q.1, p.2)∥
id       └──┘                       
src      └──┘                        
typ      └──┘                       
doc      └──┘
st   ───────────────────────────────────────
330        ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : norm_add_le_of_le (hC _ _) (hC _ _)
id                                                └───────────────┘           └┘
src                                                  └───────────────┘
typ                                               └───────────────┘           └┘
st   ────────────────────────────────────────────────────────────────────────────────────
331      ... ≤ C * ∥p∥ * ∥q∥ + C * ∥q∥ * ∥p∥ : by apply_rules [add_le_add, mul_le_mul, norm_nonneg,
id                                                            └────────┘  └────────┘  └─────────┘
src                                              └───────────┘└────────┘└┘└────────┘└┘└─────────┘└─
typ                                              └───────────┘└────────┘└┘└────────┘└┘└─────────┘└─
doc                                               └───────────┘          └┘          └┘           └─
txt                                               └───────────┘          └┘          └┘           └─
par                                               └───────────┘          └┘          └┘           └─
pid                                                          └┘          └┘          └┘           └─
st   ───────────────────────────────────────────┘└──────────────────────────────────────────────────
332        le_of_lt Cpos, le_refl, le_max_left, le_max_right, mul_nonneg, norm_nonneg, norm_nonneg,
id         └──────┘ └──┘  └─────┘  └─────────┘  └──────────┘  └────────┘  └─────────┘  └─────────┘
src  ─────┘└──────┘    └┘└─────┘└┘└─────────┘└┘└──────────┘└┘└────────┘└┘└─────────┘└┘└─────────┘└─
typ  ─────┘└──────┘└──┘└┘└─────┘└┘└─────────┘└┘└──────────┘└┘└────────┘└┘└─────────┘└┘└─────────┘└─
doc  ─────┘            └┘       └┘           └┘            └┘          └┘           └┘           └─
txt  ─────┘            └┘       └┘           └┘            └┘          └┘           └┘           └─
par  ─────┘            └┘       └┘           └┘            └┘          └┘           └┘           └─
pid  ─────┘            └┘       └┘           └┘            └┘          └┘           └┘           └─
st   ───────────────────────────────────────────────────────────────────────────────────────────────
333        norm_nonneg]
id         └─────────┘
src  ─────┘└─────────┘└─
typ  ─────┘└─────────┘└─
doc  ─────┘           └─
txt  ─────┘           └─
par  ─────┘           └─
pid  ─────┘           
st   ───────────────────
334      ... = (C + C) * ∥p∥ * ∥q∥ : by ring },
src  ───┘                               └───┘
typ  ───┘                               └───┘
doc  ───┘                               └───┘
txt  ───┘                               └───┘
par  ───┘                               └───┘
pid  ───┘                                   
st   ───┘└────────────────────────────┘└────┘└──
335  end
st   ──┘
336  
337  end bilinear_map